1. $A$ : Type
\\[0ex]2. $f$ : $A$$\rightarrow$($A$ + Top)
\\[0ex]3. $n$ : $\mathbb{Z}$
\\[0ex]4. 0 $<$ $n$
\\[0ex]5. $\forall$$y$:$A$. ($\uparrow$isl($f$\^{}$n$ {-} 1($y$))) $\Rightarrow$ ($\forall$$m$:$\mathbb{N}$. ($m$ $\leq$ ($n$ {-} 1)) $\Rightarrow$ ($\uparrow$isl($f$\^{}$m$($y$))))
\\[0ex]6. $y$ : $A$
\\[0ex]7. $m$ : $\mathbb{N}$
\\[0ex]8. $m$ $\leq$ $n$
\\[0ex]9. $\neg$($m$ = 0)
\\[0ex]$\vdash$  ($\uparrow$isl($f$\^{}$n$ {-} 1 o $f$\^{}1  ($y$))) $\Rightarrow$ ($\uparrow$isl($f$\^{}$m$ {-} 1 o $f$\^{}1  ($y$)))